  \documentclass{beamer}

%\usepackage{pgfpages}
%\setbeameroption{show notes}
%\setbeameroption{show notes on second screen=right}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm, amsfonts} 
\usepackage{textcomp}
\usepackage{stmaryrd}

%\usepackage[latin1]{inputenc}
%\usepackage[T1]{fontenc}
%\usepackage{pgfpages}

\usepackage{times}
\usepackage{xspace}

\usepackage[english]{babel}
\usepackage{url}

\usepackage{wrapfig}
\usepackage{macro}

\usepackage{color}
\newcommand{\emphcolor}[1]{\textcolor{magenta}{#1}\xspace}

\usepackage{iwona}

\title[\rnd]{Reaction networks with delays applied to toxicity analysis}
\subtitle{Joint work with Hanna Klaudel and Franck Delaplace}
\author[Cinzia Di Giusto]{\parbox[t]{6cm}{\hfill Cinzia Di Giusto\hfill\ \\\hbox{} \hfill{\tiny Universit\'e d'Evry--Val d'Essonne, IBISC}\hfill\hbox{}}\\\ }

%{Cinzia Di Giusto\\ {\tiny Universit\'e d'Evry--Val d'Essonne, IBISC}}
%\institute[IBISC]{Universit\'e d'Evry--Val d'Essonne, IBISC}

\date[]{BioPPN 2014}
  

\setbeamertemplate{navigation symbols}{} 

\usetheme{progressbar}

%\usecolortheme{crane}
%\useoutertheme{progressbar}
%\useinnertheme{progressbar}
%\usefonttheme{progressbar}

%\usetheme{progressbar}

\usepackage{setspace}

\newcommand{\putat}[3]{\begin{picture}(0,0)(0,0)\put(#1,#2){#3}\end{picture}}

\newcommand{\emphcolorb}[1]{\textcolor{blue}{#1}\xspace}


%red, gray,
%orange,
%green, white, pink,
%blue, darkgray,
%cyan,	magenta,	yellow,	black, lightgray,	brown,	lime,	olive,
%purple,


\progressbaroptions{titlepage=picture, imagename= images/cmaina.jpg, headline=sections,frametitle=picture-nosection }




\begin{document}

\begin{frame}
 \titlepage
\end{frame}

\progressbaroptions{imagename= images/logo.png}
\section{Motivation}

 
\begin{frame}
 \frametitle{The SYNBIOTIC project}
\centering
\includegraphics[width=0.6\textwidth]{schema.pdf}

\end{frame}


\begin{frame}
 \frametitle{Motivation}
 

 \begin{itemize}
  \item \emph{Main goal}: design of artificial bio-systems
  \vspace{0.3cm}
  \item \emph{How}: development of computer-aided tools
  \vspace{0.3cm}
  \item \emph{What}: specification and  analysis of  cellular regulation networks \\
  (i.e., genetic and signalization networks and metabolic pathways)
  \end{itemize}

\end{frame}





\progressbaroptions{imagename= images/cmaina.jpg}

\begin{frame}
 \frametitle{Requirements}
 
 We want to build a model where: 
 \vspace{0.3cm}
 \begin{itemize}
  \item different regulatory networks can be expressed
  \vspace{0.3cm}
  \item safety properties can be guaranteed 
 \end{itemize}
 
 
 
 \begin{block}{Safety}
  \begin{itemize}
   \item in general $\Rightarrow $ nothing bad can happen
   \vspace{0.3cm}
   \item in a bio-framework $\Rightarrow $ the system do not exhibit toxic behaviors

  \end{itemize}
 \end{block}

% 
%  \begin{block}{}
%  \begin{center}
%   We look to discretized models!
%  \end{center}
%   \end{block}

 \end{frame}
 
 
 
\progressbaroptions{imagename= images/toxic.jpeg}
\begin{frame}
 \frametitle{Toxicology}
 
 \begin{itemize}
  %\item  \emph{Toxicology} = the adverse effects of the exposures to chemicals on living entities

  \item  The \emph{toxicity process} is 
a sequence of physiological events that causes the abnormal behavior of a living
organism with respect to its healthy state. 
\vspace{0.2cm}

\item Healthy physiological states generally
correspond to \emph{homeostasis}. 
 \vspace{0.2cm}
 \item Toxicity highly depends on the exposure time and the thresholds dosage
delimiting the ranges of safe and hazardous effects.
\end{itemize}

\vspace{0.2cm}
\begin{definition}[Toxicity]
Toxicity is the  deregulation of the homeostasis processes
\end{definition}

\end{frame}

\progressbaroptions{imagename= images/Sugar.jpg}

\begin{frame}
 \frametitle{Blood glucose regulation}
 
 \begin{columns}[b]
  \begin{column}{0.5\textwidth}
 \begin{center}
 \includegraphics[width=\textwidth]{images/glucose.pdf} 
 \end{center}
  \end{column}
  \begin{column}{0.5\textwidth}
 \begin{itemize}
  \item Glucose regulation is a homeostatic process.
  \item Glycemia is regulated by insulin and glucagon. 
  \item Assimilation of sugars vs aspartame. 
  \end{itemize}
  
  \end{column}
  
 \end{columns}

 
 
 
  \pause
  
  \vspace{0.5cm}
  \begin{block}{Toxic!}
  \centering
   Assimilation of food (even if it contains aspartame) should
calm hunger and induce satiety, not the opposite!
  \end{block}

 

 \end{frame}
 
\section{\rnd}

\progressbaroptions{imagename= images/cmaina.jpg}
\begin{frame}
 \frametitle{Features}
 
 Our model features
 \vspace{0.5cm}
 \begin{itemize}
  \item An explicit notion of discrete time 
  \vspace{0.5cm}
  \item Species with expression levels and decay
  \vspace{0.5cm}
  \item Reactions with duration
 \end{itemize}

 
 \pause
 
 \begin{block}{\rnd}
  \centering
  An \rnd network is  a set of species \res governed by
a set of reactions \RS
 \end{block}

\end{frame}
 

\begin{frame}
 \frametitle{Species}

 \begin{itemize}
  \item Species have a finite number  $\setlev_s$ of  \emph{expression} levels.
  \vspace{0.2cm}
  \item Each species $s$ is initialized at   level $\level{s}$ and  
   it decays gradually as  time passes by. 
  \vspace{0.2cm}
  \item Duration  of  decay  vary among levels: $$\life_s:[0..\setlev_s-1] \to \nat^+ \cup \{\omega \}.$$
$\life_s(0) = \omega $. 
 \end{itemize}

 
\end{frame}

\begin{frame}
 \frametitle{Reactions}
 
 \begin{itemize}
  \item Reactions govern evolution of species $$
\rho ::= \ A_{\rho} \ ; \ I_{\rho} \xrightarrow{\Delta} R_{\rho}$$
 \item $A_{\rho}$, $I_{\rho}$  are sets of pairs $(s, \level{s})$ 
\vspace{0.2cm} 
 \item $R_{\rho}$ is a set of pairs $(s, \pm n)$
 \vspace{0.2cm}
 \item  Each reaction has a \emph{response time} $$\dur: \RS \to \nat^+$$  
 Time required for yielding increase (+) and/or decrease (-) of  levels of results.  
 \end{itemize}

\end{frame}

\begin{frame}
 \frametitle{Dynamics}
 
 
A reaction of response time $\dur$ can take place if
\vspace{0.2cm}
\begin{itemize}
 \item  each activator/reactant stays at least at a given level 
 \item each involved inhibitor is at most at a given level 
\end{itemize}
during the whole reaction time. 

\vspace{0.2cm}
\begin{itemize}
 \item \emph{Outcome:} the level
of results of the reaction can be increased or decreased. 

\end{itemize}


\end{frame}

\begin{frame}
 \frametitle{Formalization}
 \begin{center}
  The dynamics of \rnd is formalized using high-level Petri nets. 
 \end{center}

 
 \begin{itemize}
  \item Time is explicitly represented.
  \vspace{0.2cm}
  \item Places: Species + 1 place for time
  \vspace{0.2cm}
  \item Transition: Reaction + 1 transition for time
 \end{itemize}

 \end{frame}
%  
%  \begin{frame}
%  \frametitle{High-level Petri nets}
%  \begin{columns}[b]
% \begin{column}{0.5\textwidth}
%   \begin{tikzpicture}[scale=0.8, node distance=1.5cm,>=stealth',bend angle=45,auto]
% 
%  \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=5mm]
%  \tikzstyle{transition}=[rectangle,thick,draw=black!75,
%  			 fill=black!20,minimum size=5mm]
%  \tikzstyle{every token}=[font=\small]
% 
%   \node [place, label = left: $q_1$] at (0,1.5) (Q1){$7$};
%   \node [place, label=left:$q_2$]at (0,-1.5)  (Q2){$5$};
%   \node [place, label = right: $q_3$] at (1.5,0) (Q3){};
%   
%   \node [transition] (t) [  label={[red] left:$\begin{array}{c}
%                                                 x>y \\ \wedge \\ x'=x+y
%                                                \end{array}$}] at (0,0) {$t$}
%    edge [pre]    node[right] {$x$}    (Q1)
%    edge [pre]    node[right] {$y$}    (Q2)
%    edge [post]   node[above]{$x'$}    (Q3);
% \end{tikzpicture}  
% \end{column}
% \begin{column}{0.5\textwidth}
% 
% \begin{tikzpicture}[scale=0.8, node distance=1.5cm,>=stealth',bend angle=45,auto]
% 
%  \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=5mm]
%  \tikzstyle{transition}=[rectangle,thick,draw=black!75,
%  			 fill=black!20,minimum size=5mm]
%  \tikzstyle{every token}=[font=\small]
% 
%   \node [place, label = left: $q_1$] at (0,1.5) (Q1){};
%   \node [place, label=left:$q_2$]at (0,-1.5)  (Q2){};
%   \node [place, label = right: $q_3$] at (1.5,0) (Q3){12};
%   
%   \node [transition] (t) [  label={[red] left:$\begin{array}{c}
%                                                 x>y \\ \wedge \\ x'=x+y
%                                                \end{array}$}] at (0,0) {$t$}
%    edge [pre]    node[right] {$x$}    (Q1)
%    edge [pre]    node[right] {$y$}    (Q2)
%    edge [post]   node[above]{$x'$}    (Q3);
% \end{tikzpicture} 
% \end{column}  
%  \end{columns}
% 
%   
%  \end{frame}
% 
%  
%  
 
 \begin{frame}
  \frametitle{Places}
 

 \begin{itemize}
  \item We assume a unique discrete global clock that starts at zero and always shows the current date (timestamp). 
\vspace{0.2cm}
\item Each species is represented by a place
\vspace{0.2cm}
  \item The state of a species $s$ is a tuple $\tuple{\bool_s, \refr_s, \birth_s}$ 
\vspace{0.2cm}  
\begin{itemize}

  \item $\bool_s$ stores  the current   level; 
  \item $\refr_s$ is a timestamp recording the last date when the  level has been  updated; 
  \item $\birth_s$ is a tuple of timestamps with $\setlev_s$ fields; 
\end{itemize}

  \end{itemize}

\end{frame}

\begin{frame}
 \frametitle{Transitions -- 1}
 
 \rnd networks can evolve in two ways:
 \vspace{0.2cm}
\begin{enumerate}


\item  as effect of an enabled reaction $\rho$
 \vspace{0.2cm}

  \item as an effect of the clock: 


\end{enumerate}

\end{frame}

\begin{frame}
\frametitle{Transition: reaction}

\begin{columns}
\begin{column}{0.5\textwidth}

Transition guard:
 $$
\begin{array}{l}
  w < z  \wedge  w' = z \quad \wedge \\
 \bigwedge_{(a, \level{a}) \in A_{\rho}}(\lev_a\geq \level{a} \wedge z - \birth[\level{a}] \geq \dur(\rho) )  \quad \wedge\\
 \bigwedge_{(i, \level{i}) \in I_{\rho}}(\lev_i < \level{i} \wedge z - \birth[\level{i}] \geq \dur(\rho) )  \quad  
\end{array}
 $$

 \vspace{0.2cm}
 
Result:  a result $r$ at level $\lev_r$ and the clock at time $t$  
$$ 
\begin{array}{l}
(r, +1) \\ 
\tuple{\lev_r, \refr_r, \birth_r} \to \tuple{\lev_r + 1, t, \birth_r\sub{t}{\lev_r +1}}\\
(r, -1) \\ 
\tuple{\lev_r, \refr_r, \birth_r} \to \tuple{\lev_r - 1, t, \birth_r\sub{t}{\lev_r }}
\end{array}
$$
\end{column}
\begin{column}{0.5\textwidth}
\begin{center}
\includegraphics[width=0.9\textwidth]{reaction.png} 
\end{center}

\end{column} 
\end{columns}



\end{frame}
\begin{frame}
 \frametitle{Transitions -- Clock}
 
 \begin{enumerate}
 \setcounter{enumi}{1}
  \item as an effect of the clock: 
  \begin{itemize}
   \item The timestamp $t$ stored in the clock is incremented by one ($t+1$). 
   \item A species may stay at  level $\lev$ for $\life(\lev)$ time units. 
Decay happens as soon as the interval $\life(\lev)$ is elapsed , 
$$\tuple{\lev, \refr, \birth} \to \tuple{\lev - 1, t+1, \birth\sub{t+1}{\lev }}$$
  \end{itemize}


 \end{enumerate}

\begin{center}
\includegraphics[width=0.5\textwidth]{clock.png}
\end{center}
 
 
\end{frame}

% 
% \begin{frame}
%  \begin{example}
% 
% Suppose  a species with 5 expressions levels:
% $$
% \life(4) = 3 \quad \life(3) = 1 \quad  \life(2) = 2 \quad  \life(1) = 4 \quad  \life(0) = \omega.
% $$
% The species is initialized at  level 3 ($ \tuple{3, 0, [0,0,0,0,0]}$): 
% $$
% \begin{array}{ll}
%  \text{init} & \tuple{3, 0, [0,0,0,0,0]}  \\
%  \text{time +  decay} & \tuple{2, 1, [0,0,0,1,0]} \\
%   \text{time} & \tuple{2, 1, [0,0,0,1,0]}\\
%   \text{time + decay} & \tuple{1, 3, [0,0,3,1,0]} \\
%  \text{time x 2} & \tuple{1, 3, [0,0,3,1,0]}\\
%  \text{a reaction augments } & \tuple{2, 5, [0,0,5,1,0]}\\
%   \text{time} & \tuple{2, 5, [0,0,5,1,0]}\\
%    \text{a reaction reduces }& \tuple{1, 6, [0,0,6,1,0]}. 
% \end{array}
% $$
% \end{example}
% 
% \end{frame}


\begin{frame}
 \frametitle{Glucose regulation -- 1 }
 The set of species involved:
 $$ \begin{array}{lll}
      Sugar &\setlev_{sugar}=\{0,1\} & \life_{sugar}(1)=2 \\
      Aspartame \ &\setlev_{aspartame}=\{0,1\} & \life_{aspartame}(1)=2 \\
%  & Neurotransmitter \  &\setlev_{NT}=\{0,1\} & \life_{NT}(1)=2 \\
   Glycemia &\setlev_{glycemia}=\{0,1,2,3\} \ & \life_{glycemia}(1)=8 \\
  && \life_{glycemia}(2)=8\\
  && \life_{glycemia}(3)=8\\
   Glucagon &\setlev_{glucagon}=\{0,1\} & \life_{glucagon}(1)=3\\
    Insulin &\setlev_{insulin}=\{0,1,2\} & \life_{insulin}(1)=3\\
  && \life_{insulin}(2)=3
    \end{array}
$$

\end{frame}

\begin{frame}
\frametitle{Glucose regulation -- 2}
\begin{center}
\includegraphics[width=0.7\textwidth]{schemaglu.png}
\end{center}


\end{frame}


\begin{frame}
\frametitle{Glucose regulation -- 3}

 The set of reactions:
 
$$\begin{array}{l|c|c|c|l}
 \rho_k & Activators \ A_k & Inhibitors \ I_k & Results \ R_k &  \dur_k \\
\hline
  \rho_1 \ & \{(Sugar,1)\} &\emptyset &\{(Insulin,+),\\
  &&& (Glycemia,+)\} & 1\\
  \rho_2 & \{(Aspartame,1)\}& \emptyset &\{(Insulin,+)\} & 1\\
  \rho_3 & \emptyset &\{(Glycemia,1)\}& \{(Glucagon,+)\} &1\\
 % (\rho_4) & \{(Glycemia,1)\} &\{(Glycemia,2)\}& \{(NT,+)\} &1\\
 % (\rho_5) & \{(Glycemia,2)\} &\{(Glycemia,3)\}& \{(NT,-)\} &1\\
  \rho_4 & \{(Glycemia,3)\}& \emptyset& \{(Insulin,+)\} &1\\
  \rho_5 & \{(Insulin,2)\} & \emptyset &\{(Glycemia,-)\} &2\\
  \rho_6 & \{(Insulin,1), &&&\\
           & (Glycemia,3)\} & \emptyset &\{(Glycemia,-)\} &2\\
  \rho_7 & \{(Insulin,1)\} & \{ (Glycemia,2)\} &\{(Glycemia,-)\} &2\\
  \rho_{8} & \{(Glucagon,1)\} &\emptyset &\{(Glycemia,+)\} &2 %\ {\qed}
   \end{array}
 $$

\end{frame}


\begin{frame}
 \frametitle{Observation}
 
 \begin{itemize}

  \item Decay and reactions are different types of behaviors
 
\vspace{0.2cm}

\item Decay is synchronous\\
it corresponds to an abstraction of the action of the environment

\vspace{0.2cm}

\item  Reactions are asynchronous\\
their duration corresponds to the time required to observe an effect 

\vspace{0.2cm}


  \item Execution time vs Simulation time\\
  More reactions are enabled less probable is the execution of time

 \end{itemize}

 
 
 
\end{frame}


\section{Toxicity analysis}

\begin{frame}
 \frametitle{Toxicity analysis}

\begin{itemize}
 \item  \rnd can be  used to detect and predict toxic behaviors related to the  dynamics of bio-molecular networks. 
\vspace{0.2cm}
\item We resort to temporal logics and model checking techniques.
\vspace{0.2cm}
\item We use computation tree logic (CTL) 
\vspace{0.2cm}
\item We provide an abstraction of \rnd into Kripke structures
\end{itemize}
\end{frame}

% \begin{frame}
%  \frametitle{Kripke Stucture}
% 
% \begin{definition}[Kripke structure]
% Let $A$ be a set of atomic formulae, a \emph{Kripke structure} over $A$ is a tuple $K = (V, v_0, \longrightarrow, \lab)$ where 
% \begin{itemize}
%  \item $V$ is a finite set of states, 
%  \item $v_0\in V$ is the initial state,  
%  \item $\longrightarrow \subset V \times V$ is a left total transition relation,
%  \item $\lab$ is the labeling  function on states $\lab: V \to 2^{A}$. 
% 
% \end{itemize}
% \end{definition}
% \end{frame}
% 
% 
% \begin{frame}
%  \frametitle{Temporal logic -- CTL}
% 
% 
% 
% \begin{definition}[CTL]
% Let $a \in A$ be an atomic proposition, a CTL formula is defined as: 
% $$
% \begin{array}{ll}
%  \varphi::= &\bot \mid a \mid \neg \varphi \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid \varphi \rightarrow \varphi \\
%  & \esiste \x \varphi \mid \esiste \globally \varphi \mid \esiste (\varphi  \until \varphi) \mid \esiste \finally \varphi \mid \all \globally \varphi \mid \all \finally \varphi
% \end{array}
%  $$
% \end{definition}
% 
% \begin{itemize}
%  \item Atomic formulae are pairs of species and  levels: \\$A = \{(s, \level{s}) \mid  s\in \res\}$, for instance $(Glucose,2)$. 
% 
% \end{itemize}
% 
% 
% 
% \end{frame}

\begin{frame}
 \frametitle{Examples of questions}

\begin{block}{}
\centering
 We are  interested in checking whether the inner equilibrium of an organism is maintained when administrating drugs or applying stressors.
\end{block}

\vspace{0.5cm}

Toxicology properties can be classified into:
\begin{enumerate}
 \item   properties  checking for the appearance  of  \emph{symptoms}, 

\item properties characterizing \emph{causal relations} between events. 

\end{enumerate}



\end{frame}

% \begin{frame}
%  \frametitle{Glucose regulation --1}
% 
% \begin{block}{Symptoms:}
%  Is it possible to have an anomalous decrease of glucose levels in blood (revealing hypoglycemia)? 
% $$\esiste \finally (Glycemia, 0)$$
% \end{block}
% 
% \end{frame}
% 
% 
% \begin{frame}
%  \frametitle{Glucose regulation -- 2}
% 
% \begin{block}{Mode-of-action:}
%  Recalling that the blood glucose regulation process normally maintains  glycemia at equilibrium (level $2$), does it exist an abnormal behavior leading to hypoglycemia?
% $$\esiste (\esiste \finally (Glycemia, 2) ~\until~ (\esiste \finally (Glycemia, 0)))$$
% \end{block}
% 
% \end{frame}

\begin{frame}
 \frametitle{Glucose regulation}

\begin{block}{Causality:}
Does assimilation of sweeteners cause hypoglycemia? 
$$\begin{array}{c}
\esiste \finally [((Sugar, 1) \vee (Aspartame, 1)) \wedge (Glycemia, 1)] \rightarrow  \\
\all \finally (Glycemia,2)  
  \end{array}
 $$ 
\end{block}

\end{frame}

\begin{frame}
 \frametitle{Paths for glucose regulation}

$$\begin{array}{c}
\esiste \finally [((Sugar, 1) \vee (Aspartame, 1)) \wedge (Glycemia, 1)] \rightarrow  \\
\all \finally (Glycemia,2)  
  \end{array}
 $$ 

\begin{itemize}
 \item Path that satisfies
\end{itemize}
$$
{\footnotesize
\begin{array}{l}
(Sugar, 1), (Aspartame, 0), (Glycemia, 1), (Insulin, 0), (Glucagon, 0) \xrightarrow{\rho_1}\\
(Sugar, 1), (Aspartame, 0), \mathbf{(Glycemia, 2)}, (Insulin, 1), (Glucagon, 0) 
\end{array}}
 $$

\begin{itemize}
 \item Path that contradicts
\end{itemize}
$$
{\footnotesize
\begin{array}{l}
 (Sugar, 0), (Aspartame, 1), (Glycemia, 1), (Insulin, 0), (Glucagon, 0) \xrightarrow{\rho_2} \\ 
 (Sugar, 0), (Aspartame, 1), (Glycemia, 1), (Insulin, 1), (Glucagon, 0) \xrightarrow{\rho_7} \\
 (Sugar, 0), (Aspartame, 0), \mathbf{(Glycemia, 0)}, (Insulin, 1), (Glucagon, 0)
\end{array}}
 $$
\end{frame}
% 
% 
% \begin{frame}
%  \frametitle{Abstraction -- Intuitions}
%  \begin{itemize}
%   \item  \rnd networks have an unbounded state space as the clock can be incremented unboundedly. 
% 
% \item Changes in the status of species are referred to discrete intervals of time
% 
% \item  For each species,  we store the difference between the actual value of the clock and the timestamp. 
% 
% \item Once this value is greater than the maximum time needed to perform a reaction,  its actual value is irrelevant and it can be bounded by the greatest duration of reactions $D = \max\{\dur(\rho) \mid \rho \in \RS\}$. 
% 
% \end{itemize}
% \end{frame}
% 
% \begin{frame}
% \frametitle{Abstraction -- Species  }
% 
% The abstraction of a species $s$ is:
% $$
% \enc{\tuple{\lev_s, \refr_s, \birth_s}} = 
% \begin{cases}
% \tuple{\lev_s, \omega, \birth'_s}  &\text{if } \lev_s = 0\\
% \tuple{\lev_s, (z-\refr_s), \birth'_s}  & \text{otherwise}
% \end{cases}
% $$
% where $\birth'_s[k]=\min((z-\birth_s[k]), D)$ for all $k \in [0..\setlev_s-1]$.
% 
% \end{frame}
% 
% \begin{frame}
% \frametitle{Abstraction -- Kripke structure}
% 
% The encoding of a \rnd network $(\res, \RS)$ into a Kripke structure,  $\enc{(\res, \RS)}=(V, v_0, \longrightarrow, \lab)$, is  
% 
% \begin{itemize}
% 
%  \item $V$ is a set of tuples $v= (v(s_1), \dots ,v(s_n), v(\rho_1), \dots, v(\rho_m))$. \\
% For each $v(s)$ we take all possible combinations of values in  
% $$
% \begin{array}{ll}
% \{\tuple{\lev_s, \refr_s, \birth_s} \mid &\lev_s \in [0..\setlev_s-1], \\
% &  \refr_s = \omega \text{ if } \lev_s=0  \text{ or } \refr_s \in [0..\life_s(\lev_s)] \text{ if } \lev_s \neq 0,\\
% & \birth_s[k] \in [0..D]\text{ for } k\in [0..\setlev_s-1]\}.
% \end{array}
% $$% where $\life_s(\lev_s)$ may be different for each level $\lev_s$. 
% For $v(\rho)$ we take  values in $\{0,1\}$.
% 
% \item $v_0 = (v(s_1), \dots ,v(s_n),v(\rho_1), \dots, v(\rho_m))$ is:\\ for all $s_j \in \res$,   $v_0(s_j) = \tuple{\level{s_j}, 0, 0^{\setlev_{s_j}}}$ and for all $\rho_k \in \RS$, $v_0(\rho_k) = 1$ .
% 
% 
% \end{itemize}
% 
% 
% 
% 
% 
% \end{frame}
% 
% 
% \begin{frame}
% \frametitle{Abstraction -- Kripke structure}
% 
% The set of transitions $\longrightarrow \subseteq V \times V$  is:
% 
% \begin{enumerate}[{Item} 1.]
%  \item Encoding of the clock transition: \\
%  for each $v\in V$ there exists $v'\in V$ and $v \longrightarrow v'$ such that:
%  $$
% v'(s_j)=
% \begin{cases}
% \tuple{\lev_{s_j}, \omega, \inc{D}{\birth_{s_j}}} & \text{if } \lev_{s_j} =0\\
% \tuple{\lev_{s_j}, \refr_{s_j} +1, \inc{D}{\birth_{s_j}}} & \text{if } \lev_{s_j} \neq 0  \wedge \refr_{s_j}+1 < \life_{s_j}(\lev_{s_j})\\
% \tuple{\lev_{s_j}-1, 0, \inc{D}{\birth_{s_j}}\sub{0}{\lev_{s_j}} } & \text{otherwise.}
% \end{cases}
% $$
% for $s_j\in \res$ and $v'(\rho_k)= 1$ for all $\rho_k \in \RS$.
% \end{enumerate}
% \end{frame}
% 
% \begin{frame}
% \frametitle{Abstraction -- Kripke structure}
% 
% \begin{enumerate}[{Item} 2.]
% 
% \item Encoding of reaction transitions:\\
% for all $\rho \in \RS$ and for all $v\in V$ such that
% \begin{itemize}
%  \item $\forall (r, \level{r})\in R$ with $v(r) = \tuple{\lev_r, \refr_r, \birth_r}$: $ \lev_r \geq \level{r} \wedge \birth_r[\level{r}] \geq \dur(\rho)$ and
% \item $\forall (i,\level{i})\in I$ with $v(i) = \tuple{\lev_i, \refr_i, \birth_i}$: $\lev_i < \level{i} \wedge \birth_i[\level{i}] \geq \dur(\rho)$ and
%  \item  $v(\rho) = 1$;
% \end{itemize}
% there exists $v' \in V$ and $v \longrightarrow v'$ such that 
% \begin{itemize}
%  \item $\forall (p, +) \in P$ with  $v(p) = \tuple{\lev_p, \refr_p, \birth_p}$: if $\lev_p = \setlev_p -1$ then $v'(p) = \tuple{\lev_p, 0, \birth_p}$, otherwise  $v'(p) = \tuple{\lev_p+1, 0, \birth_p\sub{0}{\lev_p +1}}$ 
%  \item $\forall (p, -) \in P$ with $v(p) = \tuple{\lev_p, \refr_p, \birth_p}$: if $\lev_p = 0$ then $v'(p) = \tuple{\lev_p, \omega, \birth_p}$, otherwise  $v'(p) = \tuple{\lev_p-1, 0, \birth_p\sub{0}{\lev_p}}$
% \item $v'(\rho) = 0$;
% \end{itemize}
% %\item for each $v\in V$ such that there is no $v' \in V$, such that $v \longrightarrow v'$ we add a new transition $v \longrightarrow v$.
% 
% \end{enumerate}
% 
% 
% \end{frame}
% 
% 
%  



\begin{frame}
 \frametitle{Sound and completeness}

% \begin{itemize}
%  
%  \item the labeling function $\lab$ is, for each $v \in V$: $$\lab(v)= \{ (s_j, l) \mid s_j \in \res, v(s_j) = \tuple{\lev_{s_j}, \refr_{s_j}, \birth_{s_j}} \text{ and } 0 \leq l \leq l_{s_j} \}.$$
% \end{itemize} 

 
 
\begin{theorem}
Given an \rnd network $(\res, \RS)$, its encoding into 
\begin{itemize}
 \item Kripke structures
 \item Timed Automata
\end{itemize}
  is sound and complete.
\end{theorem}

\end{frame}



\section{Conclusions}
\begin{frame}
 \frametitle{Summing up}
 \begin{itemize}
  \item  \rnd, a high-level Petri net framework  for cellular regulation networks.
  \vspace{0.2cm}
  \item Species that  can degrade as time passes by governed by a set of reactions. 
\vspace{0.2cm}

\item Toxicity properties  can be expressed via a  temporal logic.
\vspace{0.2cm}

\item Properties can be  verified thanks to a
sound and complete abstraction. 

 \end{itemize}
 \end{frame}

\begin{frame}
 \frametitle{Final remarks}
 \begin{itemize}
  \item Comparison with stochastic models à la Gillespie
  \vspace{0.2cm}
  \item Refinement of the abstraction 
  \vspace{0.2cm}
  \item Implementation: Snakes, Snoopy  + Marcie
 \end{itemize}

 
\end{frame}




\begin{frame}
 \titlepage
\end{frame}


\end{document}
